Termination w.r.t. Q proof of /tmp/tmpI7qEmq/qsortlast.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

Q is empty.

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → APPEND(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
QSORT(cons(x, xs)) → QSORT(filterlow(last(cons(x, xs)), cons(x, xs)))
QSORT(cons(x, xs)) → FILTERLOW(last(cons(x, xs)), cons(x, xs))
QSORT(cons(x, xs)) → LAST(cons(x, xs))
QSORT(cons(x, xs)) → QSORT(filterhigh(last(cons(x, xs)), cons(x, xs)))
QSORT(cons(x, xs)) → FILTERHIGH(last(cons(x, xs)), cons(x, xs))
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
FILTERLOW(n, cons(x, xs)) → GE(n, x)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
FILTERHIGH(n, cons(x, xs)) → GE(x, n)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
GE(s(x), s(y)) → GE(x, y)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → APPEND(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
QSORT(cons(x, xs)) → QSORT(filterlow(last(cons(x, xs)), cons(x, xs)))
QSORT(cons(x, xs)) → FILTERLOW(last(cons(x, xs)), cons(x, xs))
QSORT(cons(x, xs)) → LAST(cons(x, xs))
QSORT(cons(x, xs)) → QSORT(filterhigh(last(cons(x, xs)), cons(x, xs)))
QSORT(cons(x, xs)) → FILTERHIGH(last(cons(x, xs)), cons(x, xs))
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
FILTERLOW(n, cons(x, xs)) → GE(n, x)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
FILTERHIGH(n, cons(x, xs)) → GE(x, n)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
GE(s(x), s(y)) → GE(x, y)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 6 SCCs with 6 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))

R is empty.
The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(x, xs), ys) → APPEND(xs, ys)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(x, xs), ys) → APPEND(xs, ys)

R is empty.
The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(x, xs), ys) → APPEND(xs, ys)

From the DPs we obtained the following set of size-change graphs:

APPEND(cons(x, xs), ys) → APPEND(xs, ys)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

R is empty.
The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

From the DPs we obtained the following set of size-change graphs:

GE(s(x), s(y)) → GE(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

From the DPs we obtained the following set of size-change graphs:

FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF1(true, n, x, xs) → FILTERLOW(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2
IF1(false, n, x, xs) → FILTERLOW(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterhigh(last(cons(x, xs)), cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(filterlow(last(cons(x, xs)), cons(x, xs)))

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterhigh(last(cons(x, xs)), cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(filterlow(last(cons(x, xs)), cons(x, xs)))

The TRS R consists of the following rules:

last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterhigh(last(cons(x, xs)), cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(filterlow(last(cons(x, xs)), cons(x, xs)))

The TRS R consists of the following rules:

last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.

This DP could be deleted by the Induction-Processor:
QSORT(cons(x', xs')) → QSORT(filterhigh(last(cons(x', xs')), cons(x', xs')))

This order was computed:
Polynomial interpretation [POLO]:

POL(0) = 0
POL(QSORT(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(false) = 3
POL(filterhigh(x₁, x₂)) = x₂
POL(filterlow(x₁, x₂)) = x₂
POL(ge(x₁, x₂)) = 3
POL(if1(x₁, x₂, x₃, x₄)) = 1 + x₃ + x₄
POL(if2(x₁, x₂, x₃, x₄)) = 1 + x₃ + x₄
POL(last(x₁)) = 3 + 2·x₁
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 2

At least one of these decreasing rules is always used after the deleted DP:
if2(true, n722, x1032, xs632) → filterhigh(n722, xs632)

The following formula is valid:
z0:sort[a36].(¬(z0 =nil)→filterhigh'(last(z0 ), z0 )=true)

The transformed set:
if2'(true, n72, x103, xs63) → true
filterhigh'(n81, cons(x115, xs71)) → if2'(ge(x115, n81), n81, x115, xs71)
if2'(false, n90, x127, xs79) → filterhigh'(n90, xs79)
filterhigh'(n99, nil) → false
last(cons(x', nil)) → x'
last(cons(x8, cons(y0, xs3))) → last(cons(y0, xs3))
if1(true, n12, x20, xs11) → filterlow(n12, xs11)
filterlow(n21, cons(x32, xs19)) → if1(ge(n21, x32), n21, x32, xs19)
ge(x44, 0) → true
ge(0, s(x56)) → false
ge(s(x68), s(y11)) → ge(x68, y11)
if1(false, n54, x80, xs48) → cons(x80, filterlow(n54, xs48))
filterlow(n63, nil) → nil
if2(true, n72, x103, xs63) → filterhigh(n72, xs63)
filterhigh(n81, cons(x115, xs71)) → if2(ge(x115, n81), n81, x115, xs71)
if2(false, n90, x127, xs79) → cons(x127, filterhigh(n90, xs79))
filterhigh(n99, nil) → nil
last(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](nil, nil) → true
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                            ↳ QTRS

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterlow(last(cons(x, xs)), cons(x, xs)))

The TRS R consists of the following rules:

last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                            ↳ QTRS

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterlow(last(cons(x, xs)), cons(x, xs)))

The TRS R consists of the following rules:

last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ Induction-Processor

                            ↳ QTRS

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterlow(last(cons(x, xs)), cons(x, xs)))

The TRS R consists of the following rules:

last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.

This DP could be deleted by the Induction-Processor:
QSORT(cons(x', xs')) → QSORT(filterlow(last(cons(x', xs')), cons(x', xs')))

This order was computed:
Polynomial interpretation [POLO]:

POL(0) = 2
POL(QSORT(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(false) = 0
POL(filterlow(x₁, x₂)) = x₂
POL(ge(x₁, x₂)) = 0
POL(if1(x₁, x₂, x₃, x₄)) = 1 + 2·x₃ + 2·x₄
POL(last(x₁)) = x₁
POL(nil) = 2
POL(s(x₁)) = 0
POL(true) = 0

At least one of these decreasing rules is always used after the deleted DP:
if1(true, n5'', x15'', xs6'') → filterlow(n5'', xs6'')

The following formula is valid:
z0:sort[a24].(¬(z0 =nil)→filterlow'(last(z0 ), z0 )=true)

The transformed set:
if1'(true, n5, x15, xs6) → true
filterlow'(n10, cons(x24, xs11)) → if1'(ge(n10, x24), n10, x24, xs11)
if1'(false, n27, x60, xs28) → filterlow'(n27, xs28)
filterlow'(n32, nil) → false
last(cons(x', nil)) → x'
last(cons(x6, cons(y0, xs1))) → last(cons(y0, xs1))
if1(true, n5, x15, xs6) → filterlow(n5, xs6)
filterlow(n10, cons(x24, xs11)) → if1(ge(n10, x24), n10, x24, xs11)
ge(x33, 0) → true
ge(0, s(x42)) → false
ge(s(x51), s(y11)) → ge(x51, y11)
if1(false, n27, x60, xs28) → cons(x60, filterlow(n27, xs28))
filterlow(n32, nil) → nil
last(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ Induction-Processor

                                        ↳ AND

                                          ↳ QDP

                                            ↳ PisEmptyProof

                                          ↳ QTRS

                            ↳ QTRS

Q DP problem:
P is empty.
The TRS R consists of the following rules:

last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ Induction-Processor

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QTRS

                                            ↳ QTRSRRRProof

                            ↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

if1'(true, n5, x15, xs6) → true
filterlow'(n10, cons(x24, xs11)) → if1'(ge(n10, x24), n10, x24, xs11)
if1'(false, n27, x60, xs28) → filterlow'(n27, xs28)
filterlow'(n32, nil) → false
last(cons(x', nil)) → x'
last(cons(x6, cons(y0, xs1))) → last(cons(y0, xs1))
if1(true, n5, x15, xs6) → filterlow(n5, xs6)
filterlow(n10, cons(x24, xs11)) → if1(ge(n10, x24), n10, x24, xs11)
ge(x33, 0) → true
ge(0, s(x42)) → false
ge(s(x51), s(y11)) → ge(x51, y11)
if1(false, n27, x60, xs28) → cons(x60, filterlow(n27, xs28))
filterlow(n32, nil) → nil
last(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

if1'(true, n5, x15, xs6) → true
filterlow'(n10, cons(x24, xs11)) → if1'(ge(n10, x24), n10, x24, xs11)
if1'(false, n27, x60, xs28) → filterlow'(n27, xs28)
filterlow'(n32, nil) → false
last(cons(x', nil)) → x'
last(cons(x6, cons(y0, xs1))) → last(cons(y0, xs1))
if1(true, n5, x15, xs6) → filterlow(n5, xs6)
filterlow(n10, cons(x24, xs11)) → if1(ge(n10, x24), n10, x24, xs11)
ge(x33, 0) → true
ge(0, s(x42)) → false
ge(s(x51), s(y11)) → ge(x51, y11)
if1(false, n27, x60, xs28) → cons(x60, filterlow(n27, xs28))
filterlow(n32, nil) → nil
last(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

Q is empty.
Used ordering:
Combined order from the following AFS and order.
if1'(x1, x2, x3, x4) = if1'(x1, x2, x3, x4)
true = true
filterlow'(x1, x2) = filterlow'(x1, x2)
cons(x1, x2) = cons(x1, x2)
ge(x1, x2) = ge(x1, x2)
false = false
nil = nil
last(x1) = last(x1)
if1(x1, x2, x3, x4) = if1(x1, x2, x3, x4)
filterlow(x1, x2) = filterlow(x1, x2)
0 = 0
s(x1) = x1
equal_bool(x1, x2) = equal_bool(x1, x2)
and(x1, x2) = and(x1, x2)
or(x1, x2) = or(x1, x2)
not(x1) = not(x1)
isa_true(x1) = isa_true(x1)
isa_false(x1) = isa_false(x1)
equal_sort[a24](x1, x2) = equal_sort[a24](x1, x2)
equal_sort[a42](x1, x2) = equal_sort[a42](x1, x2)
witness_sort[a42] = witness_sort[a42]
equal_sort[a0](x1, x2) = equal_sort[a0](x1, x2)

Recursive path order with status [RPO].
Quasi-Precedence:

[if1'₄, filterlow'₂] > [false, isa_false₁, equal_sort[a24]₂] > [ge₂, if1₄, filterlow₂] > true > cons₂
[if1'₄, filterlow'₂] > [false, isa_false₁, equal_sort[a24]₂] > and₂ > cons₂
nil > true > cons₂
last₁ > 0 > [false, isa_false₁, equal_sort[a24]₂] > [ge₂, if1₄, filterlow₂] > true > cons₂
last₁ > 0 > [false, isa_false₁, equal_sort[a24]₂] > and₂ > cons₂
equal_bool₂ > true > cons₂
or₂ > cons₂
not₁ > [false, isa_false₁, equal_sort[a24]₂] > [ge₂, if1₄, filterlow₂] > true > cons₂
not₁ > [false, isa_false₁, equal_sort[a24]₂] > and₂ > cons₂
isa_true₁ > true > cons₂
equal_sort[a42]₂ > true > cons₂
witness_sort[a42] > cons₂
equal_sort[a0]₂ > true > cons₂

Status:

witness_sort[a42]: multiset
last₁: [1]
if1'₄: [2,4,1,3]
true: multiset
or₂: [2,1]
equal_sort[a42]₂: [2,1]
and₂: [2,1]
filterlow'₂: [1,2]
0: multiset
equal_bool₂: [2,1]
equal_sort[a0]₂: [2,1]
cons₂: multiset
equal_sort[a24]₂: multiset
not₁: [1]
isa_false₁: multiset
false: multiset
filterlow₂: [1,2]
ge₂: [1,2]
nil: multiset
if1₄: [2,4,1,3]
isa_true₁: [1]

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

if1'(true, n5, x15, xs6) → true
filterlow'(n10, cons(x24, xs11)) → if1'(ge(n10, x24), n10, x24, xs11)
if1'(false, n27, x60, xs28) → filterlow'(n27, xs28)
filterlow'(n32, nil) → false
last(cons(x', nil)) → x'
last(cons(x6, cons(y0, xs1))) → last(cons(y0, xs1))
if1(true, n5, x15, xs6) → filterlow(n5, xs6)
filterlow(n10, cons(x24, xs11)) → if1(ge(n10, x24), n10, x24, xs11)
ge(x33, 0) → true
ge(0, s(x42)) → false
if1(false, n27, x60, xs28) → cons(x60, filterlow(n27, xs28))
filterlow(n32, nil) → nil
last(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ Induction-Processor

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QTRS

                                            ↳ QTRSRRRProof

                                              ↳ QTRS

                                                ↳ QTRSRRRProof

                                                ↳ QTRSRRRProof

                            ↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

ge(s(x51), s(y11)) → ge(x51, y11)
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

ge(s(x51), s(y11)) → ge(x51, y11)
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

Q is empty.
Used ordering:
Polynomial interpretation [POLO]:

POL(equal_sort[a0](x₁, x₂)) = x₁ + x₂
POL(ge(x₁, x₂)) = 2·x₁ + x₂
POL(s(x₁)) = 1 + 2·x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

ge(s(x51), s(y11)) → ge(x51, y11)
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ Induction-Processor

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QTRS

                                            ↳ QTRSRRRProof

                                              ↳ QTRS

                                                ↳ QTRSRRRProof

                                                  ↳ QTRS

                                                    ↳ RisEmptyProof

                                                    ↳ RisEmptyProof

                                                    ↳ RisEmptyProof

                                                ↳ QTRSRRRProof

                            ↳ QTRS

Q restricted rewrite system:
R is empty.
Q is empty.

The TRS R is empty. Hence, termination is trivially proven.
The TRS R is empty. Hence, termination is trivially proven.
The TRS R is empty. Hence, termination is trivially proven.
The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

ge(s(x51), s(y11)) → ge(x51, y11)
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

Q is empty.
Used ordering:
Recursive path order with status [RPO].
Quasi-Precedence:

trivial

Status:

s₁: multiset
ge₂: multiset
equal_sort[a0]₂: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

ge(s(x51), s(y11)) → ge(x51, y11)
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ Induction-Processor

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QTRS

                                            ↳ QTRSRRRProof

                                              ↳ QTRS

                                                ↳ QTRSRRRProof

                                                ↳ QTRSRRRProof

                                                  ↳ QTRS

                            ↳ QTRS

Q restricted rewrite system:
R is empty.
Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ QTRSRRRProof

Q restricted rewrite system:
The TRS R consists of the following rules:

if2'(true, n72, x103, xs63) → true
filterhigh'(n81, cons(x115, xs71)) → if2'(ge(x115, n81), n81, x115, xs71)
if2'(false, n90, x127, xs79) → filterhigh'(n90, xs79)
filterhigh'(n99, nil) → false
last(cons(x', nil)) → x'
last(cons(x8, cons(y0, xs3))) → last(cons(y0, xs3))
if1(true, n12, x20, xs11) → filterlow(n12, xs11)
filterlow(n21, cons(x32, xs19)) → if1(ge(n21, x32), n21, x32, xs19)
ge(x44, 0) → true
ge(0, s(x56)) → false
ge(s(x68), s(y11)) → ge(x68, y11)
if1(false, n54, x80, xs48) → cons(x80, filterlow(n54, xs48))
filterlow(n63, nil) → nil
if2(true, n72, x103, xs63) → filterhigh(n72, xs63)
filterhigh(n81, cons(x115, xs71)) → if2(ge(x115, n81), n81, x115, xs71)
if2(false, n90, x127, xs79) → cons(x127, filterhigh(n90, xs79))
filterhigh(n99, nil) → nil
last(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](nil, nil) → true
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

if2'(true, n72, x103, xs63) → true
filterhigh'(n81, cons(x115, xs71)) → if2'(ge(x115, n81), n81, x115, xs71)
if2'(false, n90, x127, xs79) → filterhigh'(n90, xs79)
filterhigh'(n99, nil) → false
last(cons(x', nil)) → x'
last(cons(x8, cons(y0, xs3))) → last(cons(y0, xs3))
if1(true, n12, x20, xs11) → filterlow(n12, xs11)
filterlow(n21, cons(x32, xs19)) → if1(ge(n21, x32), n21, x32, xs19)
ge(x44, 0) → true
ge(0, s(x56)) → false
ge(s(x68), s(y11)) → ge(x68, y11)
if1(false, n54, x80, xs48) → cons(x80, filterlow(n54, xs48))
filterlow(n63, nil) → nil
if2(true, n72, x103, xs63) → filterhigh(n72, xs63)
filterhigh(n81, cons(x115, xs71)) → if2(ge(x115, n81), n81, x115, xs71)
if2(false, n90, x127, xs79) → cons(x127, filterhigh(n90, xs79))
filterhigh(n99, nil) → nil
last(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](nil, nil) → true
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true

Q is empty.
Used ordering:
Combined order from the following AFS and order.
if2'(x1, x2, x3, x4) = if2'(x1, x2, x3, x4)
true = true
filterhigh'(x1, x2) = filterhigh'(x1, x2)
cons(x1, x2) = cons(x1, x2)
ge(x1, x2) = ge(x1, x2)
false = false
nil = nil
last(x1) = last(x1)
if1(x1, x2, x3, x4) = if1(x1, x2, x3, x4)
filterlow(x1, x2) = filterlow(x1, x2)
0 = 0
s(x1) = x1
if2(x1, x2, x3, x4) = if2(x1, x2, x3, x4)
filterhigh(x1, x2) = filterhigh(x1, x2)
equal_bool(x1, x2) = equal_bool(x1, x2)
and(x1, x2) = and(x1, x2)
or(x1, x2) = or(x1, x2)
not(x1) = not(x1)
isa_true(x1) = isa_true(x1)
isa_false(x1) = isa_false(x1)
equal_sort[a0](x1, x2) = equal_sort[a0](x1, x2)
equal_sort[a36](x1, x2) = equal_sort[a36](x1, x2)
equal_sort[a62](x1, x2) = equal_sort[a62](x1, x2)
witness_sort[a62] = witness_sort[a62]

Recursive path order with status [RPO].
Quasi-Precedence:

[nil, last₁, 0] > [if2'₄, filterhigh'₂, false, not₁] > true > [if2₄, filterhigh₂] > [ge₂, if1₄, filterlow₂] > cons₂
isa_true₁ > [if2'₄, filterhigh'₂, false, not₁] > true > [if2₄, filterhigh₂] > [ge₂, if1₄, filterlow₂] > cons₂
isa_false₁ > [if2'₄, filterhigh'₂, false, not₁] > true > [if2₄, filterhigh₂] > [ge₂, if1₄, filterlow₂] > cons₂
equal_sort[a36]₂ > and₂
equal_sort[a62]₂ > true > [if2₄, filterhigh₂] > [ge₂, if1₄, filterlow₂] > cons₂

Status:

if2₄: [4,2,3,1]
equal_sort[a62]₂: [2,1]
last₁: [1]
true: multiset
filterhigh'₂: [1,2]
filterhigh₂: [2,1]
or₂: [2,1]
and₂: multiset
equal_sort[a36]₂: [2,1]
if2'₄: [2,4,1,3]
0: multiset
equal_bool₂: [2,1]
equal_sort[a0]₂: [1,2]
cons₂: multiset
not₁: [1]
isa_false₁: [1]
false: multiset
filterlow₂: [2,1]
ge₂: [2,1]
nil: multiset
if1₄: [4,2,1,3]
witness_sort[a62]: multiset
isa_true₁: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

if2'(true, n72, x103, xs63) → true
filterhigh'(n81, cons(x115, xs71)) → if2'(ge(x115, n81), n81, x115, xs71)
if2'(false, n90, x127, xs79) → filterhigh'(n90, xs79)
filterhigh'(n99, nil) → false
last(cons(x', nil)) → x'
last(cons(x8, cons(y0, xs3))) → last(cons(y0, xs3))
if1(true, n12, x20, xs11) → filterlow(n12, xs11)
filterlow(n21, cons(x32, xs19)) → if1(ge(n21, x32), n21, x32, xs19)
ge(x44, 0) → true
ge(0, s(x56)) → false
if1(false, n54, x80, xs48) → cons(x80, filterlow(n54, xs48))
filterlow(n63, nil) → nil
if2(true, n72, x103, xs63) → filterhigh(n72, xs63)
filterhigh(n81, cons(x115, xs71)) → if2(ge(x115, n81), n81, x115, xs71)
if2(false, n90, x127, xs79) → cons(x127, filterhigh(n90, xs79))
filterhigh(n99, nil) → nil
last(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a36](nil, nil) → true
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ QTRSRRRProof

                                ↳ QTRS

                                  ↳ QTRSRRRProof

Q restricted rewrite system:
The TRS R consists of the following rules:

ge(s(x68), s(y11)) → ge(x68, y11)
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

ge(s(x68), s(y11)) → ge(x68, y11)
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

Q is empty.
Used ordering:
Recursive path order with status [RPO].
Quasi-Precedence:

trivial

Status:

s₁: multiset
ge₂: multiset
equal_sort[a0]₂: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

ge(s(x68), s(y11)) → ge(x68, y11)
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ QTRSRRRProof

                                ↳ QTRS

                                  ↳ QTRSRRRProof

                                    ↳ QTRS

                                      ↳ RisEmptyProof

                                      ↳ RisEmptyProof

                                      ↳ RisEmptyProof